i, x:Id, T:Type, A, B:Realizer.
R-state(A  B;i)(x)?T
~
if x  dom(R-state(A;i)) then R-state(A;i)(x)?T else R-state(B;i)(x)?T fi  

latex

Definitions	x. t(x), t  T, Top, R-state(R;i), x:A. B(x), x(s)
Lemmas	es realizer wf, top wf, fpf wf, Id wf, fpf-trivial-subtype-top, R-state wf, id-deq wf, fpf-join-cap-sq